A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))). [(I|p)?(I|p)] = I 

latex

Definitions	E, [f?g], (I|p), (I|p), AbsInterface(A), f(a), x(s), <a, b>, s = t, x:A. B(x), Dec(P), x:AB(x), Type, , ES, P  Q, P  Q, x. t(x), Top, left + right, x:A  B(x), P & Q, P  Q, , b, A, t  T, Unit, f o g  , p-co-restrict(f;p), p-restrict(f;p), False, P  Q, can-apply(f;x), p-co-filter(f), inr x , True, x:A.B(x)
Lemmas	can-apply-p-co-filter, equal-top, true wf, not wf, false wf, can-apply-p-filter, do-apply-p-filter, not functionality wrt iff, can-apply-p-restrict, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, do-apply-p-co-filter